Nuprl Lemma : bilinear_comm_elim 13,42
T:Type, pl, tm:(TTT).
Comm(T;tm)  (a, x, y:T. (a tm (x pl y)) = ((a tm x) pl (a tm y))  T)  BiLinear(T;pl;tm) 
latex

Upgen algebra 1
Definitions of StatementComm(T;op), BiLinear(T;pl;tm)
Definitions, t  T, P & Q, BiLinear(T;pl;tm), x f y, Comm(T;op), P  Q, x:A. B(x), P  Q, P  Q

origin